(1
 (
  ("(var3 stable)" 0 52)
  ("(var3 down)" 52 54)
  ("(var3 up)" 54 88)
  ("(var3 stable)" 88 164)
  ("(var3 up)" 164 169)
  ("(var3 down)" 169 179)
  ("(var3 up)" 179 182)
  ("(var3 stable)" 182 320)
  ("(var4 stable)" 0 52)
  ("(var4 up)" 52 88)
  ("(var4 stable)" 88 174)
  ("(var4 down)" 174 272)
  ("(var4 stable)" 272 320)
  ("(var1 stable)" 0 47)
  ("(var1 down)" 47 50)
  ("(var1 up)" 50 86)
  ("(var1 stable)" 86 320)
  ("(var2 stable)" 0 72)
  ("(var2 down)" 72 74)
  ("(var2 up)" 74 196)
  ("(var2 stable)" 196 320)
 )
)
(2
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 70)
  ("(var3 stable)" 70 139)
  ("(var3 up)" 139 144)
  ("(var3 down)" 144 154)
  ("(var3 up)" 154 159)
  ("(var3 stable)" 159 286)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 63)
  ("(var4 stable)" 63 150)
  ("(var4 down)" 150 246)
  ("(var4 stable)" 246 286)
  ("(var1 stable)" 0 36)
  ("(var1 up)" 36 67)
  ("(var1 stable)" 67 286)
  ("(var2 stable)" 0 56)
  ("(var2 down)" 56 58)
  ("(var2 stable)" 58 88)
  ("(var2 up)" 88 148)
  ("(var2 down)" 148 150)
  ("(var2 up)" 150 183)
  ("(var2 stable)" 183 286)
 )
)
(3
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 113)
  ("(var3 stable)" 113 115)
  ("(var3 up)" 115 117)
  ("(var3 stable)" 117 195)
  ("(var3 up)" 195 204)
  ("(var3 down)" 204 215)
  ("(var3 up)" 215 219)
  ("(var3 stable)" 219 366)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 104)
  ("(var4 stable)" 104 106)
  ("(var4 up)" 106 108)
  ("(var4 down)" 108 110)
  ("(var4 stable)" 110 245)
  ("(var4 down)" 245 317)
  ("(var4 stable)" 317 366)
  ("(var1 stable)" 0 75)
  ("(var1 up)" 75 111)
  ("(var1 stable)" 111 366)
  ("(var2 stable)" 0 98)
  ("(var2 down)" 98 100)
  ("(var2 up)" 100 238)
  ("(var2 stable)" 238 366)
 )
)
(4
 (
  ("(var3 stable)" 0 48)
  ("(var3 up)" 48 80)
  ("(var3 stable)" 80 173)
  ("(var3 up)" 173 176)
  ("(var3 down)" 176 187)
  ("(var3 stable)" 187 189)
  ("(var3 up)" 189 194)
  ("(var3 stable)" 194 338)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 57)
  ("(var4 stable)" 57 59)
  ("(var4 up)" 59 82)
  ("(var4 stable)" 82 215)
  ("(var4 down)" 215 294)
  ("(var4 stable)" 294 338)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 86)
  ("(var1 stable)" 86 338)
  ("(var2 stable)" 0 73)
  ("(var2 down)" 73 75)
  ("(var2 stable)" 75 99)
  ("(var2 up)" 99 122)
  ("(var2 down)" 122 124)
  ("(var2 up)" 124 203)
  ("(var2 stable)" 203 338)
 )
)
(5
 (
  ("(var3 stable)" 0 89)
  ("(var3 up)" 89 128)
  ("(var3 stable)" 128 193)
  ("(var3 up)" 193 197)
  ("(var3 down)" 197 207)
  ("(var3 stable)" 207 209)
  ("(var3 up)" 209 211)
  ("(var3 stable)" 211 338)
  ("(var4 stable)" 0 90)
  ("(var4 up)" 90 125)
  ("(var4 stable)" 125 212)
  ("(var4 down)" 212 214)
  ("(var4 stable)" 214 219)
  ("(var4 down)" 219 300)
  ("(var4 stable)" 300 338)
  ("(var1 stable)" 0 89)
  ("(var1 up)" 89 120)
  ("(var1 stable)" 120 338)
  ("(var2 stable)" 0 108)
  ("(var2 down)" 108 110)
  ("(var2 up)" 110 233)
  ("(var2 stable)" 233 338)
 )
)
(6
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 117)
  ("(var3 stable)" 117 197)
  ("(var3 up)" 197 201)
  ("(var3 down)" 201 209)
  ("(var3 up)" 209 214)
  ("(var3 stable)" 214 347)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 112)
  ("(var4 down)" 112 114)
  ("(var4 up)" 114 116)
  ("(var4 stable)" 116 238)
  ("(var4 down)" 238 303)
  ("(var4 stable)" 303 347)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 82)
  ("(var1 stable)" 82 84)
  ("(var1 up)" 84 115)
  ("(var1 stable)" 115 347)
  ("(var2 stable)" 0 102)
  ("(var2 down)" 102 104)
  ("(var2 stable)" 104 141)
  ("(var2 up)" 141 230)
  ("(var2 down)" 230 233)
  ("(var2 up)" 233 235)
  ("(var2 stable)" 235 347)
 )
)
(7
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 75)
  ("(var3 stable)" 75 143)
  ("(var3 up)" 143 148)
  ("(var3 down)" 148 158)
  ("(var3 stable)" 158 160)
  ("(var3 up)" 160 163)
  ("(var3 stable)" 163 286)
  ("(var4 stable)" 0 44)
  ("(var4 up)" 44 85)
  ("(var4 stable)" 85 168)
  ("(var4 down)" 168 170)
  ("(var4 up)" 170 172)
  ("(var4 down)" 172 174)
  ("(var4 stable)" 174 176)
  ("(var4 down)" 176 180)
  ("(var4 stable)" 180 182)
  ("(var4 down)" 182 247)
  ("(var4 stable)" 247 286)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 69)
  ("(var1 stable)" 69 286)
  ("(var2 stable)" 0 65)
  ("(var2 up)" 65 190)
  ("(var2 stable)" 190 286)
 )
)
(8
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 86)
  ("(var3 stable)" 86 166)
  ("(var3 up)" 166 170)
  ("(var3 down)" 170 179)
  ("(var3 up)" 179 183)
  ("(var3 stable)" 183 320)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 90)
  ("(var4 stable)" 90 180)
  ("(var4 down)" 180 278)
  ("(var4 stable)" 278 320)
  ("(var1 stable)" 0 54)
  ("(var1 up)" 54 85)
  ("(var1 stable)" 85 320)
  ("(var2 stable)" 0 72)
  ("(var2 down)" 72 76)
  ("(var2 stable)" 76 109)
  ("(var2 up)" 109 176)
  ("(var2 down)" 176 178)
  ("(var2 up)" 178 196)
  ("(var2 stable)" 196 320)
 )
)
(9
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 52)
  ("(var3 stable)" 52 55)
  ("(var3 up)" 55 84)
  ("(var3 stable)" 84 154)
  ("(var3 up)" 154 161)
  ("(var3 down)" 161 169)
  ("(var3 up)" 169 171)
  ("(var3 stable)" 171 306)
  ("(var4 stable)" 0 50)
  ("(var4 up)" 50 85)
  ("(var4 stable)" 85 166)
  ("(var4 down)" 166 263)
  ("(var4 stable)" 263 269)
  ("(var4 down)" 269 271)
  ("(var4 stable)" 271 306)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 81)
  ("(var1 stable)" 81 306)
  ("(var2 stable)" 0 72)
  ("(var2 down)" 72 74)
  ("(var2 up)" 74 195)
  ("(var2 down)" 195 199)
  ("(var2 up)" 199 201)
  ("(var2 stable)" 201 306)
 )
)
(10
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 108)
  ("(var3 stable)" 108 199)
  ("(var3 up)" 199 205)
  ("(var3 down)" 205 216)
  ("(var3 up)" 216 221)
  ("(var3 stable)" 221 369)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 76)
  ("(var4 stable)" 76 79)
  ("(var4 up)" 79 120)
  ("(var4 stable)" 120 241)
  ("(var4 down)" 241 243)
  ("(var4 up)" 243 246)
  ("(var4 down)" 246 334)
  ("(var4 stable)" 334 369)
  ("(var1 stable)" 0 76)
  ("(var1 up)" 76 113)
  ("(var1 stable)" 113 369)
  ("(var2 stable)" 0 98)
  ("(var2 down)" 98 102)
  ("(var2 up)" 102 207)
  ("(var2 down)" 207 209)
  ("(var2 up)" 209 248)
  ("(var2 stable)" 248 367)
  ("(var2 down)" 367 369)
 )
)
(11
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 96)
  ("(var3 stable)" 96 183)
  ("(var3 up)" 183 190)
  ("(var3 down)" 190 200)
  ("(var3 up)" 200 204)
  ("(var3 stable)" 204 350)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 97)
  ("(var4 stable)" 97 228)
  ("(var4 down)" 228 324)
  ("(var4 stable)" 324 350)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 96)
  ("(var1 stable)" 96 348)
  ("(var1 up)" 348 350)
  ("(var2 stable)" 0 83)
  ("(var2 down)" 83 85)
  ("(var2 up)" 85 217)
  ("(var2 stable)" 217 221)
  ("(var2 down)" 221 223)
  ("(var2 up)" 223 225)
  ("(var2 stable)" 225 350)
 )
)
(12
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 101)
  ("(var3 stable)" 101 184)
  ("(var3 up)" 184 189)
  ("(var3 down)" 189 198)
  ("(var3 up)" 198 203)
  ("(var3 stable)" 203 345)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 96)
  ("(var4 stable)" 96 234)
  ("(var4 down)" 234 339)
  ("(var4 stable)" 339 345)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 97)
  ("(var1 stable)" 97 345)
  ("(var2 stable)" 0 88)
  ("(var2 down)" 88 90)
  ("(var2 stable)" 90 126)
  ("(var2 up)" 126 191)
  ("(var2 stable)" 191 193)
  ("(var2 up)" 193 222)
  ("(var2 down)" 222 224)
  ("(var2 up)" 224 228)
  ("(var2 stable)" 228 345)
 )
)
(13
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 53)
  ("(var3 stable)" 53 56)
  ("(var3 up)" 56 82)
  ("(var3 stable)" 82 155)
  ("(var3 up)" 155 159)
  ("(var3 down)" 159 168)
  ("(var3 up)" 168 175)
  ("(var3 stable)" 175 291)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 85)
  ("(var4 stable)" 85 170)
  ("(var4 down)" 170 257)
  ("(var4 stable)" 257 291)
  ("(var1 stable)" 0 52)
  ("(var1 up)" 52 81)
  ("(var1 stable)" 81 291)
  ("(var2 stable)" 0 71)
  ("(var2 down)" 71 73)
  ("(var2 up)" 73 188)
  ("(var2 stable)" 188 291)
 )
)
(14
 (
  ("(var3 stable)" 0 68)
  ("(var3 up)" 68 70)
  ("(var3 stable)" 70 72)
  ("(var3 up)" 72 102)
  ("(var3 stable)" 102 189)
  ("(var3 up)" 189 195)
  ("(var3 down)" 195 206)
  ("(var3 up)" 206 211)
  ("(var3 stable)" 211 349)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 106)
  ("(var4 down)" 106 108)
  ("(var4 stable)" 108 203)
  ("(var4 down)" 203 315)
  ("(var4 stable)" 315 349)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 100)
  ("(var1 stable)" 100 349)
  ("(var2 stable)" 0 93)
  ("(var2 down)" 93 95)
  ("(var2 stable)" 95 132)
  ("(var2 up)" 132 134)
  ("(var2 down)" 134 136)
  ("(var2 up)" 136 227)
  ("(var2 stable)" 227 349)
 )
)
(15
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 76)
  ("(var3 stable)" 76 151)
  ("(var3 up)" 151 155)
  ("(var3 down)" 155 165)
  ("(var3 up)" 165 169)
  ("(var3 stable)" 169 299)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 75)
  ("(var4 stable)" 75 171)
  ("(var4 down)" 171 174)
  ("(var4 up)" 174 176)
  ("(var4 down)" 176 248)
  ("(var4 stable)" 248 250)
  ("(var4 down)" 250 263)
  ("(var4 stable)" 263 299)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 71)
  ("(var1 stable)" 71 299)
  ("(var2 stable)" 0 63)
  ("(var2 down)" 63 65)
  ("(var2 stable)" 65 99)
  ("(var2 up)" 99 193)
  ("(var2 stable)" 193 299)
 )
)
(16
 (
  ("(var3 stable)" 0 45)
  ("(var3 up)" 45 80)
  ("(var3 stable)" 80 156)
  ("(var3 up)" 156 159)
  ("(var3 down)" 159 169)
  ("(var3 stable)" 169 171)
  ("(var3 up)" 171 174)
  ("(var3 stable)" 174 304)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 81)
  ("(var4 down)" 81 83)
  ("(var4 up)" 83 85)
  ("(var4 stable)" 85 177)
  ("(var4 down)" 177 265)
  ("(var4 stable)" 265 304)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 81)
  ("(var1 stable)" 81 304)
  ("(var2 stable)" 0 66)
  ("(var2 down)" 66 68)
  ("(var2 stable)" 68 103)
  ("(var2 up)" 103 192)
  ("(var2 stable)" 192 304)
 )
)
(17
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 86)
  ("(var3 down)" 86 89)
  ("(var3 up)" 89 121)
  ("(var3 stable)" 121 204)
  ("(var3 up)" 204 211)
  ("(var3 down)" 211 220)
  ("(var3 up)" 220 226)
  ("(var3 stable)" 226 373)
  ("(var4 stable)" 0 86)
  ("(var4 up)" 86 130)
  ("(var4 stable)" 130 242)
  ("(var4 down)" 242 309)
  ("(var4 stable)" 309 311)
  ("(var4 down)" 311 352)
  ("(var4 stable)" 352 373)
  ("(var1 stable)" 0 78)
  ("(var1 up)" 78 119)
  ("(var1 stable)" 119 373)
  ("(var2 stable)" 0 110)
  ("(var2 down)" 110 112)
  ("(var2 up)" 112 217)
  ("(var2 down)" 217 219)
  ("(var2 up)" 219 255)
  ("(var2 stable)" 255 373)
 )
)
(18
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 106)
  ("(var3 stable)" 106 185)
  ("(var3 up)" 185 189)
  ("(var3 down)" 189 198)
  ("(var3 up)" 198 206)
  ("(var3 stable)" 206 333)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 106)
  ("(var4 stable)" 106 200)
  ("(var4 down)" 200 229)
  ("(var4 stable)" 229 233)
  ("(var4 down)" 233 299)
  ("(var4 stable)" 299 333)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 103)
  ("(var1 stable)" 103 333)
  ("(var2 stable)" 0 94)
  ("(var2 down)" 94 98)
  ("(var2 up)" 98 219)
  ("(var2 down)" 219 221)
  ("(var2 up)" 221 224)
  ("(var2 stable)" 224 333)
 )
)
(19
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 68)
  ("(var3 stable)" 68 144)
  ("(var3 up)" 144 149)
  ("(var3 down)" 149 158)
  ("(var3 up)" 158 162)
  ("(var3 stable)" 162 286)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 74)
  ("(var4 stable)" 74 155)
  ("(var4 down)" 155 247)
  ("(var4 stable)" 247 286)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 69)
  ("(var1 stable)" 69 286)
  ("(var2 stable)" 0 59)
  ("(var2 down)" 59 63)
  ("(var2 up)" 63 167)
  ("(var2 down)" 167 169)
  ("(var2 up)" 169 171)
  ("(var2 stable)" 171 286)
 )
)
(20
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 91)
  ("(var3 stable)" 91 182)
  ("(var3 up)" 182 186)
  ("(var3 down)" 186 196)
  ("(var3 up)" 196 201)
  ("(var3 stable)" 201 340)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 100)
  ("(var4 stable)" 100 202)
  ("(var4 down)" 202 297)
  ("(var4 stable)" 297 299)
  ("(var4 down)" 299 301)
  ("(var4 stable)" 301 340)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 95)
  ("(var1 stable)" 95 340)
  ("(var2 stable)" 0 83)
  ("(var2 down)" 83 87)
  ("(var2 up)" 87 131)
  ("(var2 stable)" 131 135)
  ("(var2 up)" 135 184)
  ("(var2 down)" 184 186)
  ("(var2 up)" 186 220)
  ("(var2 stable)" 220 340)
 )
)
(21
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 60)
  ("(var3 down)" 60 62)
  ("(var3 up)" 62 90)
  ("(var3 stable)" 90 174)
  ("(var3 up)" 174 176)
  ("(var3 down)" 176 184)
  ("(var3 up)" 184 191)
  ("(var3 stable)" 191 319)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 91)
  ("(var4 stable)" 91 177)
  ("(var4 down)" 177 179)
  ("(var4 up)" 179 181)
  ("(var4 down)" 181 278)
  ("(var4 stable)" 278 319)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 93)
  ("(var1 stable)" 93 319)
  ("(var2 stable)" 0 82)
  ("(var2 down)" 82 84)
  ("(var2 stable)" 84 121)
  ("(var2 up)" 121 217)
  ("(var2 stable)" 217 319)
 )
)
(22
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 106)
  ("(var3 stable)" 106 188)
  ("(var3 up)" 188 194)
  ("(var3 down)" 194 204)
  ("(var3 up)" 204 208)
  ("(var3 stable)" 208 345)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 110)
  ("(var4 stable)" 110 206)
  ("(var4 down)" 206 208)
  ("(var4 up)" 208 210)
  ("(var4 down)" 210 308)
  ("(var4 stable)" 308 345)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 112)
  ("(var1 stable)" 112 345)
  ("(var2 stable)" 0 97)
  ("(var2 down)" 97 99)
  ("(var2 up)" 99 233)
  ("(var2 stable)" 233 345)
 )
)
(23
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 78)
  ("(var3 stable)" 78 165)
  ("(var3 up)" 165 170)
  ("(var3 down)" 170 184)
  ("(var3 up)" 184 186)
  ("(var3 stable)" 186 328)
  ("(var4 stable)" 0 40)
  ("(var4 up)" 40 87)
  ("(var4 stable)" 87 186)
  ("(var4 down)" 186 308)
  ("(var4 up)" 308 310)
  ("(var4 stable)" 310 326)
  ("(var4 up)" 326 328)
  ("(var1 stable)" 0 47)
  ("(var1 up)" 47 86)
  ("(var1 stable)" 86 328)
  ("(var2 stable)" 0 66)
  ("(var2 down)" 66 70)
  ("(var2 up)" 70 114)
  ("(var2 stable)" 114 116)
  ("(var2 up)" 116 200)
  ("(var2 stable)" 200 328)
 )
)
(24
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 114)
  ("(var3 stable)" 114 190)
  ("(var3 up)" 190 194)
  ("(var3 down)" 194 205)
  ("(var3 up)" 205 210)
  ("(var3 stable)" 210 333)
  ("(var4 stable)" 0 76)
  ("(var4 down)" 76 78)
  ("(var4 up)" 78 113)
  ("(var4 stable)" 113 228)
  ("(var4 down)" 228 289)
  ("(var4 stable)" 289 333)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 82)
  ("(var1 stable)" 82 85)
  ("(var1 up)" 85 115)
  ("(var1 stable)" 115 333)
  ("(var2 stable)" 0 102)
  ("(var2 down)" 102 104)
  ("(var2 stable)" 104 132)
  ("(var2 up)" 132 228)
  ("(var2 stable)" 228 333)
 )
)
(25
 (
  ("(var3 stable)" 0 31)
  ("(var3 up)" 31 66)
  ("(var3 stable)" 66 69)
  ("(var3 up)" 69 71)
  ("(var3 stable)" 71 150)
  ("(var3 up)" 150 155)
  ("(var3 down)" 155 166)
  ("(var3 up)" 166 171)
  ("(var3 stable)" 171 305)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 73)
  ("(var4 stable)" 73 171)
  ("(var4 down)" 171 173)
  ("(var4 up)" 173 175)
  ("(var4 down)" 175 268)
  ("(var4 stable)" 268 305)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 72)
  ("(var1 stable)" 72 305)
  ("(var2 stable)" 0 58)
  ("(var2 down)" 58 60)
  ("(var2 up)" 60 190)
  ("(var2 stable)" 190 305)
 )
)
(26
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 92)
  ("(var3 stable)" 92 168)
  ("(var3 up)" 168 171)
  ("(var3 stable)" 171 173)
  ("(var3 down)" 173 182)
  ("(var3 up)" 182 186)
  ("(var3 stable)" 186 313)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 97)
  ("(var4 stable)" 97 189)
  ("(var4 down)" 189 274)
  ("(var4 stable)" 274 313)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 91)
  ("(var1 stable)" 91 313)
  ("(var2 stable)" 0 81)
  ("(var2 down)" 81 83)
  ("(var2 up)" 83 215)
  ("(var2 stable)" 215 313)
 )
)
(27
 (
  ("(var3 stable)" 0 68)
  ("(var3 up)" 68 110)
  ("(var3 stable)" 110 173)
  ("(var3 up)" 173 178)
  ("(var3 down)" 178 186)
  ("(var3 stable)" 186 188)
  ("(var3 up)" 188 192)
  ("(var3 stable)" 192 317)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 95)
  ("(var4 down)" 95 97)
  ("(var4 up)" 97 99)
  ("(var4 stable)" 99 184)
  ("(var4 down)" 184 277)
  ("(var4 stable)" 277 317)
  ("(var1 stable)" 0 68)
  ("(var1 up)" 68 97)
  ("(var1 stable)" 97 317)
  ("(var2 stable)" 0 87)
  ("(var2 down)" 87 89)
  ("(var2 up)" 89 206)
  ("(var2 stable)" 206 317)
 )
)
(28
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 101)
  ("(var3 stable)" 101 181)
  ("(var3 up)" 181 186)
  ("(var3 down)" 186 194)
  ("(var3 up)" 194 198)
  ("(var3 stable)" 198 327)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 111)
  ("(var4 stable)" 111 185)
  ("(var4 down)" 185 187)
  ("(var4 stable)" 187 193)
  ("(var4 up)" 193 195)
  ("(var4 down)" 195 282)
  ("(var4 stable)" 282 327)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 104)
  ("(var1 down)" 104 108)
  ("(var1 stable)" 108 327)
  ("(var2 stable)" 0 92)
  ("(var2 down)" 92 94)
  ("(var2 up)" 94 226)
  ("(var2 stable)" 226 327)
 )
)
(29
 (
  ("(var3 stable)" 0 47)
  ("(var3 up)" 47 79)
  ("(var3 stable)" 79 157)
  ("(var3 up)" 157 162)
  ("(var3 down)" 162 173)
  ("(var3 up)" 173 176)
  ("(var3 stable)" 176 306)
  ("(var3 up)" 306 308)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 77)
  ("(var4 stable)" 77 172)
  ("(var4 down)" 172 301)
  ("(var4 stable)" 301 308)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 79)
  ("(var1 stable)" 79 308)
  ("(var2 stable)" 0 67)
  ("(var2 down)" 67 69)
  ("(var2 up)" 69 106)
  ("(var2 down)" 106 108)
  ("(var2 up)" 108 166)
  ("(var2 stable)" 166 168)
  ("(var2 up)" 168 204)
  ("(var2 stable)" 204 308)
 )
)
(30
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 73)
  ("(var3 stable)" 73 150)
  ("(var3 up)" 150 155)
  ("(var3 down)" 155 166)
  ("(var3 up)" 166 170)
  ("(var3 stable)" 170 306)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 69)
  ("(var4 down)" 69 71)
  ("(var4 up)" 71 73)
  ("(var4 stable)" 73 168)
  ("(var4 down)" 168 261)
  ("(var4 stable)" 261 306)
  ("(var1 stable)" 0 32)
  ("(var1 up)" 32 69)
  ("(var1 stable)" 69 306)
  ("(var2 stable)" 0 59)
  ("(var2 down)" 59 61)
  ("(var2 up)" 61 160)
  ("(var2 down)" 160 162)
  ("(var2 up)" 162 201)
  ("(var2 stable)" 201 306)
 )
)
(31
 (
  ("(var3 stable)" 0 42)
  ("(var3 up)" 42 78)
  ("(var3 stable)" 78 162)
  ("(var3 up)" 162 168)
  ("(var3 down)" 168 178)
  ("(var3 up)" 178 183)
  ("(var3 stable)" 183 326)
  ("(var4 stable)" 0 48)
  ("(var4 up)" 48 81)
  ("(var4 stable)" 81 176)
  ("(var4 down)" 176 292)
  ("(var4 stable)" 292 326)
  ("(var1 up)" 0 2)
  ("(var1 stable)" 2 41)
  ("(var1 up)" 41 81)
  ("(var1 stable)" 81 326)
  ("(var2 stable)" 0 68)
  ("(var2 down)" 68 70)
  ("(var2 stable)" 70 109)
  ("(var2 up)" 109 215)
  ("(var2 stable)" 215 326)
 )
)
(32
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 81)
  ("(var3 stable)" 81 158)
  ("(var3 up)" 158 164)
  ("(var3 down)" 164 172)
  ("(var3 up)" 172 177)
  ("(var3 stable)" 177 310)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 84)
  ("(var4 stable)" 84 168)
  ("(var4 down)" 168 272)
  ("(var4 stable)" 272 310)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 81)
  ("(var1 stable)" 81 310)
  ("(var2 stable)" 0 71)
  ("(var2 down)" 71 73)
  ("(var2 stable)" 73 105)
  ("(var2 up)" 105 172)
  ("(var2 stable)" 172 174)
  ("(var2 up)" 174 212)
  ("(var2 stable)" 212 310)
 )
)
(33
 (
  ("(var3 stable)" 0 40)
  ("(var3 up)" 40 61)
  ("(var3 down)" 61 63)
  ("(var3 up)" 63 74)
  ("(var3 stable)" 74 156)
  ("(var3 up)" 156 161)
  ("(var3 down)" 161 172)
  ("(var3 up)" 172 178)
  ("(var3 stable)" 178 321)
  ("(var3 up)" 321 323)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 68)
  ("(var4 down)" 68 70)
  ("(var4 up)" 70 72)
  ("(var4 stable)" 72 168)
  ("(var4 down)" 168 207)
  ("(var4 stable)" 207 209)
  ("(var4 down)" 209 297)
  ("(var4 stable)" 297 323)
  ("(var1 stable)" 0 36)
  ("(var1 up)" 36 67)
  ("(var1 stable)" 67 323)
  ("(var2 stable)" 0 58)
  ("(var2 down)" 58 65)
  ("(var2 stable)" 65 67)
  ("(var2 up)" 67 201)
  ("(var2 down)" 201 203)
  ("(var2 up)" 203 208)
  ("(var2 stable)" 208 323)
 )
)
(34
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 100)
  ("(var3 stable)" 100 163)
  ("(var3 up)" 163 167)
  ("(var3 stable)" 167 169)
  ("(var3 down)" 169 177)
  ("(var3 up)" 177 182)
  ("(var3 stable)" 182 312)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 93)
  ("(var4 stable)" 93 165)
  ("(var4 down)" 165 267)
  ("(var4 up)" 267 269)
  ("(var4 down)" 269 273)
  ("(var4 stable)" 273 312)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 87)
  ("(var1 stable)" 87 90)
  ("(var1 up)" 90 92)
  ("(var1 stable)" 92 312)
  ("(var2 stable)" 0 79)
  ("(var2 down)" 79 81)
  ("(var2 stable)" 81 114)
  ("(var2 up)" 114 202)
  ("(var2 stable)" 202 312)
 )
)
(35
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 63)
  ("(var3 stable)" 63 133)
  ("(var3 up)" 133 138)
  ("(var3 down)" 138 148)
  ("(var3 up)" 148 152)
  ("(var3 stable)" 152 272)
  ("(var4 down)" 0 2)
  ("(var4 stable)" 2 32)
  ("(var4 up)" 32 61)
  ("(var4 stable)" 61 162)
  ("(var4 down)" 162 164)
  ("(var4 up)" 164 166)
  ("(var4 down)" 166 245)
  ("(var4 stable)" 245 272)
  ("(var1 stable)" 0 32)
  ("(var1 down)" 32 34)
  ("(var1 up)" 34 64)
  ("(var1 stable)" 64 272)
  ("(var2 stable)" 0 52)
  ("(var2 down)" 52 54)
  ("(var2 stable)" 54 84)
  ("(var2 up)" 84 146)
  ("(var2 down)" 146 148)
  ("(var2 up)" 148 162)
  ("(var2 stable)" 162 272)
 )
)
(36
 (
  ("(var3 stable)" 0 81)
  ("(var3 up)" 81 130)
  ("(var3 stable)" 130 207)
  ("(var3 up)" 207 210)
  ("(var3 stable)" 210 212)
  ("(var3 down)" 212 222)
  ("(var3 up)" 222 226)
  ("(var3 stable)" 226 369)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 127)
  ("(var4 stable)" 127 218)
  ("(var4 down)" 218 329)
  ("(var4 stable)" 329 369)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 124)
  ("(var1 stable)" 124 369)
  ("(var2 stable)" 0 109)
  ("(var2 down)" 109 116)
  ("(var2 up)" 116 118)
  ("(var2 stable)" 118 124)
  ("(var2 up)" 124 126)
  ("(var2 down)" 126 128)
  ("(var2 up)" 128 236)
  ("(var2 stable)" 236 369)
 )
)
(37
 (
  ("(var3 stable)" 0 28)
  ("(var3 up)" 28 67)
  ("(var3 stable)" 67 149)
  ("(var3 up)" 149 154)
  ("(var3 down)" 154 165)
  ("(var3 up)" 165 169)
  ("(var3 stable)" 169 305)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 71)
  ("(var4 stable)" 71 164)
  ("(var4 down)" 164 255)
  ("(var4 stable)" 255 258)
  ("(var4 down)" 258 260)
  ("(var4 stable)" 260 264)
  ("(var4 down)" 264 266)
  ("(var4 stable)" 266 305)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 65)
  ("(var1 stable)" 65 305)
  ("(var2 stable)" 0 54)
  ("(var2 down)" 54 58)
  ("(var2 stable)" 58 96)
  ("(var2 up)" 96 186)
  ("(var2 stable)" 186 305)
 )
)
(38
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 62)
  ("(var3 stable)" 62 65)
  ("(var3 up)" 65 85)
  ("(var3 down)" 85 87)
  ("(var3 up)" 87 89)
  ("(var3 stable)" 89 165)
  ("(var3 up)" 165 170)
  ("(var3 down)" 170 181)
  ("(var3 up)" 181 186)
  ("(var3 stable)" 186 317)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 60)
  ("(var4 stable)" 60 65)
  ("(var4 up)" 65 93)
  ("(var4 stable)" 93 180)
  ("(var4 down)" 180 272)
  ("(var4 stable)" 272 317)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 91)
  ("(var1 stable)" 91 317)
  ("(var2 stable)" 0 80)
  ("(var2 down)" 80 82)
  ("(var2 up)" 82 215)
  ("(var2 stable)" 215 317)
 )
)
(39
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 117)
  ("(var3 stable)" 117 196)
  ("(var3 up)" 196 201)
  ("(var3 down)" 201 211)
  ("(var3 up)" 211 217)
  ("(var3 stable)" 217 351)
  ("(var4 stable)" 0 88)
  ("(var4 down)" 88 90)
  ("(var4 up)" 90 124)
  ("(var4 stable)" 124 207)
  ("(var4 down)" 207 304)
  ("(var4 stable)" 304 351)
  ("(var1 stable)" 0 89)
  ("(var1 up)" 89 120)
  ("(var1 stable)" 120 351)
  ("(var2 stable)" 0 107)
  ("(var2 down)" 107 111)
  ("(var2 up)" 111 206)
  ("(var2 stable)" 206 209)
  ("(var2 up)" 209 246)
  ("(var2 stable)" 246 351)
 )
)
(40
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 74)
  ("(var3 stable)" 74 150)
  ("(var3 up)" 150 154)
  ("(var3 down)" 154 164)
  ("(var3 up)" 164 169)
  ("(var3 stable)" 169 298)
  ("(var4 stable)" 0 44)
  ("(var4 up)" 44 81)
  ("(var4 down)" 81 83)
  ("(var4 stable)" 83 174)
  ("(var4 down)" 174 252)
  ("(var4 stable)" 252 295)
  ("(var4 up)" 295 298)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 71)
  ("(var1 stable)" 71 298)
  ("(var2 stable)" 0 64)
  ("(var2 down)" 64 66)
  ("(var2 up)" 66 103)
  ("(var2 down)" 103 105)
  ("(var2 up)" 105 195)
  ("(var2 stable)" 195 298)
 )
)
(41
 (
  ("(var3 stable)" 0 29)
  ("(var3 up)" 29 31)
  ("(var3 down)" 31 33)
  ("(var3 up)" 33 37)
  ("(var3 stable)" 37 39)
  ("(var3 up)" 39 68)
  ("(var3 stable)" 68 147)
  ("(var3 up)" 147 153)
  ("(var3 stable)" 153 155)
  ("(var3 down)" 155 165)
  ("(var3 up)" 165 170)
  ("(var3 stable)" 170 307)
  ("(var4 stable)" 0 36)
  ("(var4 up)" 36 64)
  ("(var4 down)" 64 66)
  ("(var4 stable)" 66 166)
  ("(var4 down)" 166 268)
  ("(var4 stable)" 268 305)
  ("(var4 up)" 305 307)
  ("(var1 stable)" 0 24)
  ("(var1 up)" 24 64)
  ("(var1 stable)" 64 66)
  ("(var1 up)" 66 70)
  ("(var1 stable)" 70 307)
  ("(var2 stable)" 0 55)
  ("(var2 down)" 55 57)
  ("(var2 up)" 57 161)
  ("(var2 stable)" 161 163)
  ("(var2 up)" 163 203)
  ("(var2 stable)" 203 307)
 )
)
(42
 (
  ("(var3 stable)" 0 33)
  ("(var3 up)" 33 67)
  ("(var3 stable)" 67 141)
  ("(var3 up)" 141 146)
  ("(var3 down)" 146 155)
  ("(var3 up)" 155 160)
  ("(var3 stable)" 160 282)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 70)
  ("(var4 stable)" 70 154)
  ("(var4 down)" 154 249)
  ("(var4 stable)" 249 282)
  ("(var1 stable)" 0 33)
  ("(var1 up)" 33 66)
  ("(var1 stable)" 66 282)
  ("(var2 stable)" 0 55)
  ("(var2 down)" 55 57)
  ("(var2 stable)" 57 90)
  ("(var2 up)" 90 158)
  ("(var2 stable)" 158 282)
 )
)
(43
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 107)
  ("(var3 stable)" 107 184)
  ("(var3 up)" 184 187)
  ("(var3 stable)" 187 189)
  ("(var3 down)" 189 196)
  ("(var3 up)" 196 202)
  ("(var3 stable)" 202 330)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 114)
  ("(var4 stable)" 114 194)
  ("(var4 down)" 194 280)
  ("(var4 up)" 280 282)
  ("(var4 down)" 282 286)
  ("(var4 stable)" 286 330)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 105)
  ("(var1 stable)" 105 330)
  ("(var2 stable)" 0 95)
  ("(var2 down)" 95 99)
  ("(var2 up)" 99 237)
  ("(var2 stable)" 237 330)
 )
)
(44
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 78)
  ("(var3 stable)" 78 151)
  ("(var3 up)" 151 156)
  ("(var3 down)" 156 164)
  ("(var3 up)" 164 169)
  ("(var3 stable)" 169 299)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 77)
  ("(var4 stable)" 77 182)
  ("(var4 down)" 182 259)
  ("(var4 stable)" 259 299)
  ("(var1 stable)" 0 45)
  ("(var1 up)" 45 77)
  ("(var1 stable)" 77 299)
  ("(var2 stable)" 0 69)
  ("(var2 down)" 69 71)
  ("(var2 up)" 71 199)
  ("(var2 stable)" 199 299)
 )
)
(45
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 68)
  ("(var3 stable)" 68 145)
  ("(var3 up)" 145 152)
  ("(var3 down)" 152 163)
  ("(var3 up)" 163 167)
  ("(var3 stable)" 167 302)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 69)
  ("(var4 stable)" 69 189)
  ("(var4 down)" 189 254)
  ("(var4 stable)" 254 257)
  ("(var4 down)" 257 259)
  ("(var4 stable)" 259 302)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 69)
  ("(var1 stable)" 69 302)
  ("(var2 stable)" 0 56)
  ("(var2 down)" 56 58)
  ("(var2 stable)" 58 94)
  ("(var2 up)" 94 191)
  ("(var2 stable)" 191 302)
 )
)
(46
 (
  ("(var3 stable)" 0 34)
  ("(var3 up)" 34 65)
  ("(var3 stable)" 65 141)
  ("(var3 up)" 141 145)
  ("(var3 down)" 145 156)
  ("(var3 up)" 156 163)
  ("(var3 stable)" 163 294)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 69)
  ("(var4 stable)" 69 165)
  ("(var4 down)" 165 260)
  ("(var4 stable)" 260 294)
  ("(var1 stable)" 0 36)
  ("(var1 up)" 36 64)
  ("(var1 stable)" 64 294)
  ("(var2 stable)" 0 53)
  ("(var2 down)" 53 55)
  ("(var2 stable)" 55 86)
  ("(var2 up)" 86 176)
  ("(var2 down)" 176 179)
  ("(var2 stable)" 179 294)
 )
)
(47
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 101)
  ("(var3 stable)" 101 179)
  ("(var3 up)" 179 181)
  ("(var3 down)" 181 192)
  ("(var3 up)" 192 197)
  ("(var3 stable)" 197 316)
  ("(var4 stable)" 0 65)
  ("(var4 up)" 65 105)
  ("(var4 stable)" 105 187)
  ("(var4 down)" 187 277)
  ("(var4 stable)" 277 316)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 101)
  ("(var1 stable)" 101 316)
  ("(var2 stable)" 0 92)
  ("(var2 down)" 92 96)
  ("(var2 stable)" 96 115)
  ("(var2 up)" 115 209)
  ("(var2 stable)" 209 314)
  ("(var2 down)" 314 316)
 )
)
(48
 (
  ("(var3 stable)" 0 94)
  ("(var3 up)" 94 96)
  ("(var3 stable)" 96 98)
  ("(var3 up)" 98 130)
  ("(var3 stable)" 130 209)
  ("(var3 up)" 209 214)
  ("(var3 down)" 214 224)
  ("(var3 up)" 224 228)
  ("(var3 stable)" 228 373)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 90)
  ("(var4 stable)" 90 94)
  ("(var4 up)" 94 99)
  ("(var4 stable)" 99 101)
  ("(var4 up)" 101 129)
  ("(var4 stable)" 129 251)
  ("(var4 down)" 251 253)
  ("(var4 up)" 253 256)
  ("(var4 down)" 256 260)
  ("(var4 up)" 260 262)
  ("(var4 down)" 262 330)
  ("(var4 stable)" 330 373)
  ("(var1 stable)" 0 92)
  ("(var1 up)" 92 94)
  ("(var1 stable)" 94 98)
  ("(var1 up)" 98 130)
  ("(var1 down)" 130 132)
  ("(var1 up)" 132 135)
  ("(var1 stable)" 135 373)
  ("(var2 stable)" 0 115)
  ("(var2 down)" 115 117)
  ("(var2 up)" 117 261)
  ("(var2 stable)" 261 373)
 )
)
(49
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 94)
  ("(var3 stable)" 94 172)
  ("(var3 up)" 172 175)
  ("(var3 down)" 175 185)
  ("(var3 up)" 185 192)
  ("(var3 stable)" 192 314)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 104)
  ("(var4 stable)" 104 188)
  ("(var4 down)" 188 280)
  ("(var4 stable)" 280 314)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 95)
  ("(var1 stable)" 95 314)
  ("(var2 stable)" 0 85)
  ("(var2 down)" 85 87)
  ("(var2 up)" 87 179)
  ("(var2 stable)" 179 181)
  ("(var2 up)" 181 183)
  ("(var2 down)" 183 185)
  ("(var2 up)" 185 210)
  ("(var2 stable)" 210 314)
 )
)
(50
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 113)
  ("(var3 stable)" 113 191)
  ("(var3 up)" 191 194)
  ("(var3 down)" 194 204)
  ("(var3 up)" 204 210)
  ("(var3 stable)" 210 350)
  ("(var4 stable)" 0 79)
  ("(var4 up)" 79 111)
  ("(var4 stable)" 111 209)
  ("(var4 down)" 209 309)
  ("(var4 stable)" 309 350)
  ("(var1 stable)" 0 76)
  ("(var1 up)" 76 109)
  ("(var1 stable)" 109 350)
  ("(var2 stable)" 0 98)
  ("(var2 down)" 98 100)
  ("(var2 up)" 100 240)
  ("(var2 stable)" 240 350)
 )
)
(51
 (
  ("(var3 stable)" 0 62)
  ("(var3 up)" 62 91)
  ("(var3 stable)" 91 167)
  ("(var3 up)" 167 172)
  ("(var3 down)" 172 181)
  ("(var3 stable)" 181 183)
  ("(var3 up)" 183 186)
  ("(var3 stable)" 186 320)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 60)
  ("(var4 down)" 60 62)
  ("(var4 up)" 62 83)
  ("(var4 stable)" 83 85)
  ("(var4 up)" 85 90)
  ("(var4 stable)" 90 186)
  ("(var4 down)" 186 272)
  ("(var4 stable)" 272 320)
  ("(var1 stable)" 0 58)
  ("(var1 up)" 58 90)
  ("(var1 stable)" 90 320)
  ("(var2 stable)" 0 78)
  ("(var2 down)" 78 80)
  ("(var2 up)" 80 202)
  ("(var2 stable)" 202 320)
 )
)
(52
 (
  ("(var3 stable)" 0 88)
  ("(var3 up)" 88 115)
  ("(var3 stable)" 115 117)
  ("(var3 up)" 117 119)
  ("(var3 stable)" 119 206)
  ("(var3 up)" 206 209)
  ("(var3 down)" 209 219)
  ("(var3 up)" 219 226)
  ("(var3 stable)" 226 372)
  ("(var4 stable)" 0 91)
  ("(var4 up)" 91 125)
  ("(var4 stable)" 125 223)
  ("(var4 down)" 223 225)
  ("(var4 stable)" 225 227)
  ("(var4 down)" 227 349)
  ("(var4 stable)" 349 372)
  ("(var1 stable)" 0 91)
  ("(var1 up)" 91 123)
  ("(var1 stable)" 123 372)
  ("(var2 stable)" 0 110)
  ("(var2 down)" 110 112)
  ("(var2 stable)" 112 149)
  ("(var2 up)" 149 225)
  ("(var2 stable)" 225 372)
 )
)
(53
 (
  ("(var3 stable)" 0 29)
  ("(var3 up)" 29 31)
  ("(var3 stable)" 31 34)
  ("(var3 up)" 34 61)
  ("(var3 down)" 61 63)
  ("(var3 up)" 63 65)
  ("(var3 stable)" 65 68)
  ("(var3 up)" 68 70)
  ("(var3 stable)" 70 149)
  ("(var3 up)" 149 153)
  ("(var3 down)" 153 164)
  ("(var3 up)" 164 171)
  ("(var3 stable)" 171 308)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 61)
  ("(var4 down)" 61 63)
  ("(var4 stable)" 63 162)
  ("(var4 down)" 162 255)
  ("(var4 stable)" 255 258)
  ("(var4 down)" 258 293)
  ("(var4 up)" 293 295)
  ("(var4 stable)" 295 308)
  ("(var1 stable)" 0 30)
  ("(var1 up)" 30 61)
  ("(var1 stable)" 61 63)
  ("(var1 up)" 63 65)
  ("(var1 stable)" 65 308)
  ("(var2 stable)" 0 53)
  ("(var2 down)" 53 55)
  ("(var2 stable)" 55 94)
  ("(var2 up)" 94 193)
  ("(var2 stable)" 193 308)
 )
)
(54
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 68)
  ("(var3 down)" 68 70)
  ("(var3 stable)" 70 145)
  ("(var3 up)" 145 152)
  ("(var3 down)" 152 162)
  ("(var3 up)" 162 168)
  ("(var3 stable)" 168 298)
  ("(var4 stable)" 0 2)
  ("(var4 up)" 2 4)
  ("(var4 stable)" 4 33)
  ("(var4 down)" 33 36)
  ("(var4 stable)" 36 39)
  ("(var4 up)" 39 77)
  ("(var4 stable)" 77 159)
  ("(var4 down)" 159 253)
  ("(var4 stable)" 253 256)
  ("(var4 down)" 256 260)
  ("(var4 stable)" 260 298)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 75)
  ("(var1 stable)" 75 298)
  ("(var2 stable)" 0 58)
  ("(var2 down)" 58 60)
  ("(var2 up)" 60 187)
  ("(var2 stable)" 187 298)
 )
)
(55
 (
  ("(var3 stable)" 0 102)
  ("(var3 up)" 102 132)
  ("(var3 stable)" 132 136)
  ("(var3 up)" 136 138)
  ("(var3 stable)" 138 219)
  ("(var3 up)" 219 224)
  ("(var3 down)" 224 235)
  ("(var3 stable)" 235 237)
  ("(var3 up)" 237 240)
  ("(var3 stable)" 240 387)
  ("(var4 stable)" 0 96)
  ("(var4 up)" 96 135)
  ("(var4 stable)" 135 243)
  ("(var4 down)" 243 329)
  ("(var4 stable)" 329 332)
  ("(var4 down)" 332 336)
  ("(var4 stable)" 336 387)
  ("(var1 stable)" 0 91)
  ("(var1 up)" 91 129)
  ("(var1 stable)" 129 387)
  ("(var2 stable)" 0 118)
  ("(var2 down)" 118 120)
  ("(var2 up)" 120 253)
  ("(var2 stable)" 253 387)
 )
)
(56
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 76)
  ("(var3 stable)" 76 157)
  ("(var3 up)" 157 162)
  ("(var3 down)" 162 172)
  ("(var3 up)" 172 177)
  ("(var3 stable)" 177 317)
  ("(var4 stable)" 0 40)
  ("(var4 up)" 40 75)
  ("(var4 stable)" 75 177)
  ("(var4 down)" 177 289)
  ("(var4 stable)" 289 317)
  ("(var1 stable)" 0 39)
  ("(var1 up)" 39 74)
  ("(var1 stable)" 74 317)
  ("(var2 stable)" 0 60)
  ("(var2 down)" 60 64)
  ("(var2 up)" 64 203)
  ("(var2 stable)" 203 317)
 )
)
(57
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 106)
  ("(var3 stable)" 106 188)
  ("(var3 up)" 188 192)
  ("(var3 stable)" 192 194)
  ("(var3 down)" 194 204)
  ("(var3 up)" 204 208)
  ("(var3 stable)" 208 352)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 106)
  ("(var4 stable)" 106 229)
  ("(var4 down)" 229 307)
  ("(var4 up)" 307 309)
  ("(var4 down)" 309 311)
  ("(var4 stable)" 311 350)
  ("(var4 up)" 350 352)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 104)
  ("(var1 down)" 104 106)
  ("(var1 stable)" 106 352)
  ("(var2 stable)" 0 94)
  ("(var2 down)" 94 98)
  ("(var2 up)" 98 205)
  ("(var2 stable)" 205 352)
 )
)
(58
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 104)
  ("(var3 down)" 104 108)
  ("(var3 up)" 108 112)
  ("(var3 stable)" 112 190)
  ("(var3 up)" 190 196)
  ("(var3 down)" 196 205)
  ("(var3 up)" 205 209)
  ("(var3 stable)" 209 348)
  ("(var4 stable)" 0 81)
  ("(var4 up)" 81 107)
  ("(var4 stable)" 107 212)
  ("(var4 down)" 212 303)
  ("(var4 stable)" 303 348)
  ("(var1 stable)" 0 70)
  ("(var1 down)" 70 72)
  ("(var1 up)" 72 74)
  ("(var1 stable)" 74 77)
  ("(var1 up)" 77 103)
  ("(var1 stable)" 103 348)
  ("(var2 stable)" 0 94)
  ("(var2 down)" 94 96)
  ("(var2 up)" 96 216)
  ("(var2 stable)" 216 348)
 )
)
(59
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 117)
  ("(var3 stable)" 117 193)
  ("(var3 up)" 193 199)
  ("(var3 down)" 199 209)
  ("(var3 up)" 209 213)
  ("(var3 stable)" 213 342)
  ("(var4 stable)" 0 85)
  ("(var4 up)" 85 110)
  ("(var4 stable)" 110 216)
  ("(var4 down)" 216 297)
  ("(var4 stable)" 297 300)
  ("(var4 down)" 300 302)
  ("(var4 stable)" 302 342)
  ("(var1 stable)" 0 84)
  ("(var1 down)" 84 86)
  ("(var1 up)" 86 112)
  ("(var1 stable)" 112 342)
  ("(var2 stable)" 0 104)
  ("(var2 down)" 104 106)
  ("(var2 up)" 106 227)
  ("(var2 stable)" 227 342)
 )
)
(60
 (
  ("(var3 stable)" 0 85)
  ("(var3 up)" 85 123)
  ("(var3 stable)" 123 213)
  ("(var3 up)" 213 216)
  ("(var3 down)" 216 227)
  ("(var3 up)" 227 232)
  ("(var3 stable)" 232 372)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 122)
  ("(var4 stable)" 122 233)
  ("(var4 down)" 233 325)
  ("(var4 stable)" 325 367)
  ("(var4 up)" 367 370)
  ("(var4 down)" 370 372)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 120)
  ("(var1 stable)" 120 372)
  ("(var2 stable)" 0 112)
  ("(var2 down)" 112 114)
  ("(var2 stable)" 114 155)
  ("(var2 up)" 155 254)
  ("(var2 down)" 254 256)
  ("(var2 up)" 256 258)
  ("(var2 stable)" 258 372)
 )
)
(61
 (
  ("(var3 stable)" 0 45)
  ("(var3 up)" 45 80)
  ("(var3 stable)" 80 150)
  ("(var3 up)" 150 155)
  ("(var3 down)" 155 166)
  ("(var3 up)" 166 171)
  ("(var3 stable)" 171 299)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 74)
  ("(var4 stable)" 74 185)
  ("(var4 down)" 185 256)
  ("(var4 stable)" 256 299)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 74)
  ("(var1 stable)" 74 299)
  ("(var2 stable)" 0 61)
  ("(var2 down)" 61 63)
  ("(var2 up)" 63 179)
  ("(var2 stable)" 179 299)
 )
)
(62
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 79)
  ("(var3 down)" 79 81)
  ("(var3 up)" 81 120)
  ("(var3 stable)" 120 200)
  ("(var3 up)" 200 207)
  ("(var3 down)" 207 217)
  ("(var3 up)" 217 221)
  ("(var3 stable)" 221 366)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 124)
  ("(var4 stable)" 124 215)
  ("(var4 down)" 215 318)
  ("(var4 stable)" 318 322)
  ("(var4 down)" 322 324)
  ("(var4 stable)" 324 366)
  ("(var1 stable)" 0 74)
  ("(var1 up)" 74 84)
  ("(var1 stable)" 84 86)
  ("(var1 up)" 86 111)
  ("(var1 stable)" 111 113)
  ("(var1 up)" 113 122)
  ("(var1 stable)" 122 366)
  ("(var2 stable)" 0 103)
  ("(var2 down)" 103 105)
  ("(var2 up)" 105 248)
  ("(var2 stable)" 248 366)
 )
)
(63
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 84)
  ("(var3 stable)" 84 172)
  ("(var3 up)" 172 176)
  ("(var3 stable)" 176 178)
  ("(var3 down)" 178 187)
  ("(var3 up)" 187 192)
  ("(var3 stable)" 192 334)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 85)
  ("(var4 down)" 85 87)
  ("(var4 up)" 87 93)
  ("(var4 stable)" 93 189)
  ("(var4 down)" 189 271)
  ("(var4 up)" 271 273)
  ("(var4 down)" 273 283)
  ("(var4 up)" 283 285)
  ("(var4 stable)" 285 328)
  ("(var4 up)" 328 332)
  ("(var4 down)" 332 334)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 81)
  ("(var1 stable)" 81 83)
  ("(var1 up)" 83 85)
  ("(var1 down)" 85 88)
  ("(var1 stable)" 88 334)
  ("(var2 stable)" 0 73)
  ("(var2 down)" 73 75)
  ("(var2 stable)" 75 115)
  ("(var2 up)" 115 215)
  ("(var2 down)" 215 217)
  ("(var2 stable)" 217 332)
  ("(var2 down)" 332 334)
 )
)
(64
 (
  ("(var3 stable)" 0 86)
  ("(var3 up)" 86 114)
  ("(var3 stable)" 114 187)
  ("(var3 up)" 187 192)
  ("(var3 down)" 192 203)
  ("(var3 up)" 203 208)
  ("(var3 stable)" 208 337)
  ("(var4 stable)" 0 86)
  ("(var4 up)" 86 122)
  ("(var4 down)" 122 124)
  ("(var4 stable)" 124 217)
  ("(var4 down)" 217 221)
  ("(var4 up)" 221 223)
  ("(var4 down)" 223 312)
  ("(var4 stable)" 312 337)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 114)
  ("(var1 stable)" 114 337)
  ("(var2 stable)" 0 103)
  ("(var2 down)" 103 107)
  ("(var2 stable)" 107 121)
  ("(var2 up)" 121 240)
  ("(var2 stable)" 240 337)
 )
)
(65
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 97)
  ("(var3 stable)" 97 169)
  ("(var3 up)" 169 173)
  ("(var3 down)" 173 182)
  ("(var3 up)" 182 187)
  ("(var3 stable)" 187 313)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 68)
  ("(var4 down)" 68 70)
  ("(var4 up)" 70 73)
  ("(var4 stable)" 73 75)
  ("(var4 up)" 75 95)
  ("(var4 stable)" 95 185)
  ("(var4 down)" 185 273)
  ("(var4 stable)" 273 313)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 95)
  ("(var1 stable)" 95 313)
  ("(var2 stable)" 0 88)
  ("(var2 down)" 88 90)
  ("(var2 stable)" 90 121)
  ("(var2 up)" 121 199)
  ("(var2 stable)" 199 313)
 )
)
(66
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 64)
  ("(var3 down)" 64 66)
  ("(var3 up)" 66 68)
  ("(var3 stable)" 68 148)
  ("(var3 up)" 148 153)
  ("(var3 down)" 153 161)
  ("(var3 stable)" 161 163)
  ("(var3 up)" 163 168)
  ("(var3 stable)" 168 307)
  ("(var4 stable)" 0 35)
  ("(var4 up)" 35 67)
  ("(var4 stable)" 67 181)
  ("(var4 down)" 181 260)
  ("(var4 stable)" 260 307)
  ("(var1 stable)" 0 33)
  ("(var1 up)" 33 35)
  ("(var1 down)" 35 37)
  ("(var1 up)" 37 66)
  ("(var1 stable)" 66 307)
  ("(var2 stable)" 0 55)
  ("(var2 down)" 55 57)
  ("(var2 up)" 57 152)
  ("(var2 down)" 152 154)
  ("(var2 up)" 154 192)
  ("(var2 stable)" 192 307)
 )
)
(67
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 79)
  ("(var3 stable)" 79 81)
  ("(var3 up)" 81 112)
  ("(var3 stable)" 112 186)
  ("(var3 up)" 186 189)
  ("(var3 down)" 189 199)
  ("(var3 up)" 199 202)
  ("(var3 stable)" 202 330)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 115)
  ("(var4 stable)" 115 198)
  ("(var4 down)" 198 291)
  ("(var4 stable)" 291 330)
  ("(var1 stable)" 0 83)
  ("(var1 up)" 83 112)
  ("(var1 stable)" 112 330)
  ("(var2 stable)" 0 98)
  ("(var2 down)" 98 100)
  ("(var2 up)" 100 192)
  ("(var2 down)" 192 194)
  ("(var2 up)" 194 222)
  ("(var2 stable)" 222 330)
 )
)
(68
 (
  ("(var3 stable)" 0 73)
  ("(var3 up)" 73 103)
  ("(var3 stable)" 103 180)
  ("(var3 up)" 180 185)
  ("(var3 down)" 185 193)
  ("(var3 up)" 193 199)
  ("(var3 stable)" 199 330)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 100)
  ("(var4 stable)" 100 186)
  ("(var4 down)" 186 295)
  ("(var4 stable)" 295 297)
  ("(var4 down)" 297 299)
  ("(var4 stable)" 299 330)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 101)
  ("(var1 stable)" 101 330)
  ("(var2 stable)" 0 89)
  ("(var2 down)" 89 91)
  ("(var2 stable)" 91 122)
  ("(var2 up)" 122 147)
  ("(var2 down)" 147 149)
  ("(var2 up)" 149 198)
  ("(var2 stable)" 198 330)
 )
)
(69
 (
  ("(var3 stable)" 0 33)
  ("(var3 up)" 33 69)
  ("(var3 down)" 69 71)
  ("(var3 stable)" 71 146)
  ("(var3 up)" 146 151)
  ("(var3 down)" 151 161)
  ("(var3 up)" 161 165)
  ("(var3 stable)" 165 300)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 65)
  ("(var4 stable)" 65 180)
  ("(var4 down)" 180 182)
  ("(var4 up)" 182 184)
  ("(var4 down)" 184 273)
  ("(var4 stable)" 273 300)
  ("(var1 stable)" 0 27)
  ("(var1 up)" 27 64)
  ("(var1 stable)" 64 300)
  ("(var2 stable)" 0 54)
  ("(var2 down)" 54 56)
  ("(var2 up)" 56 180)
  ("(var2 stable)" 180 300)
 )
)
(70
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 109)
  ("(var3 stable)" 109 179)
  ("(var3 up)" 179 184)
  ("(var3 down)" 184 194)
  ("(var3 up)" 194 197)
  ("(var3 stable)" 197 328)
  ("(var4 stable)" 0 72)
  ("(var4 down)" 72 74)
  ("(var4 up)" 74 102)
  ("(var4 stable)" 102 198)
  ("(var4 down)" 198 283)
  ("(var4 stable)" 283 323)
  ("(var4 up)" 323 325)
  ("(var4 stable)" 325 328)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 101)
  ("(var1 down)" 101 103)
  ("(var1 up)" 103 105)
  ("(var1 stable)" 105 328)
  ("(var2 stable)" 0 91)
  ("(var2 down)" 91 93)
  ("(var2 up)" 93 222)
  ("(var2 stable)" 222 328)
 )
)
(71
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 114)
  ("(var3 stable)" 114 190)
  ("(var3 up)" 190 194)
  ("(var3 stable)" 194 196)
  ("(var3 down)" 196 206)
  ("(var3 up)" 206 210)
  ("(var3 stable)" 210 345)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 113)
  ("(var4 stable)" 113 200)
  ("(var4 down)" 200 299)
  ("(var4 up)" 299 301)
  ("(var4 down)" 301 310)
  ("(var4 stable)" 310 345)
  ("(var1 stable)" 0 76)
  ("(var1 up)" 76 110)
  ("(var1 stable)" 110 343)
  ("(var1 up)" 343 345)
  ("(var2 stable)" 0 97)
  ("(var2 down)" 97 101)
  ("(var2 up)" 101 201)
  ("(var2 down)" 201 203)
  ("(var2 up)" 203 231)
  ("(var2 stable)" 231 345)
 )
)
(72
 (
  ("(var3 stable)" 0 79)
  ("(var3 up)" 79 109)
  ("(var3 stable)" 109 184)
  ("(var3 up)" 184 188)
  ("(var3 stable)" 188 190)
  ("(var3 down)" 190 199)
  ("(var3 up)" 199 205)
  ("(var3 stable)" 205 333)
  ("(var4 stable)" 0 81)
  ("(var4 up)" 81 111)
  ("(var4 stable)" 111 200)
  ("(var4 up)" 200 202)
  ("(var4 down)" 202 286)
  ("(var4 up)" 286 288)
  ("(var4 down)" 288 301)
  ("(var4 stable)" 301 333)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 106)
  ("(var1 stable)" 106 333)
  ("(var2 stable)" 0 99)
  ("(var2 down)" 99 101)
  ("(var2 up)" 101 216)
  ("(var2 down)" 216 218)
  ("(var2 up)" 218 220)
  ("(var2 stable)" 220 333)
 )
)
(73
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 82)
  ("(var3 up)" 82 111)
  ("(var3 stable)" 111 192)
  ("(var3 up)" 192 197)
  ("(var3 down)" 197 207)
  ("(var3 up)" 207 212)
  ("(var3 stable)" 212 346)
  ("(var4 stable)" 0 86)
  ("(var4 up)" 86 109)
  ("(var4 stable)" 109 230)
  ("(var4 down)" 230 232)
  ("(var4 stable)" 232 234)
  ("(var4 down)" 234 293)
  ("(var4 up)" 293 295)
  ("(var4 down)" 295 297)
  ("(var4 stable)" 297 344)
  ("(var4 up)" 344 346)
  ("(var1 stable)" 0 81)
  ("(var1 up)" 81 115)
  ("(var1 stable)" 115 346)
  ("(var2 stable)" 0 102)
  ("(var2 down)" 102 104)
  ("(var2 up)" 104 202)
  ("(var2 down)" 202 204)
  ("(var2 up)" 204 238)
  ("(var2 stable)" 238 346)
 )
)
(74
 (
  ("(var3 stable)" 0 25)
  ("(var3 up)" 25 27)
  ("(var3 down)" 27 29)
  ("(var3 up)" 29 31)
  ("(var3 stable)" 31 33)
  ("(var3 up)" 33 63)
  ("(var3 stable)" 63 135)
  ("(var3 up)" 135 139)
  ("(var3 down)" 139 147)
  ("(var3 up)" 147 150)
  ("(var3 stable)" 150 271)
  ("(var4 stable)" 0 28)
  ("(var4 up)" 28 66)
  ("(var4 stable)" 66 146)
  ("(var4 down)" 146 179)
  ("(var4 stable)" 179 181)
  ("(var4 down)" 181 238)
  ("(var4 stable)" 238 271)
  ("(var1 stable)" 0 28)
  ("(var1 up)" 28 62)
  ("(var1 stable)" 62 271)
  ("(var2 stable)" 0 50)
  ("(var2 down)" 50 54)
  ("(var2 up)" 54 161)
  ("(var2 stable)" 161 271)
 )
)
(75
 (
  ("(var3 up)" 0 2)
  ("(var3 stable)" 2 33)
  ("(var3 up)" 33 66)
  ("(var3 stable)" 66 149)
  ("(var3 up)" 149 154)
  ("(var3 down)" 154 164)
  ("(var3 up)" 164 166)
  ("(var3 stable)" 166 306)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 65)
  ("(var4 down)" 65 67)
  ("(var4 stable)" 67 160)
  ("(var4 down)" 160 270)
  ("(var4 stable)" 270 306)
  ("(var1 stable)" 0 34)
  ("(var1 up)" 34 65)
  ("(var1 down)" 65 67)
  ("(var1 up)" 67 69)
  ("(var1 stable)" 69 306)
  ("(var2 stable)" 0 56)
  ("(var2 down)" 56 58)
  ("(var2 up)" 58 191)
  ("(var2 stable)" 191 306)
 )
)
(76
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 104)
  ("(var3 down)" 104 106)
  ("(var3 up)" 106 108)
  ("(var3 stable)" 108 193)
  ("(var3 up)" 193 198)
  ("(var3 down)" 198 208)
  ("(var3 up)" 208 213)
  ("(var3 stable)" 213 350)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 113)
  ("(var4 stable)" 113 235)
  ("(var4 down)" 235 311)
  ("(var4 stable)" 311 350)
  ("(var1 stable)" 0 74)
  ("(var1 up)" 74 111)
  ("(var1 stable)" 111 350)
  ("(var2 stable)" 0 97)
  ("(var2 down)" 97 99)
  ("(var2 stable)" 99 129)
  ("(var2 up)" 129 205)
  ("(var2 down)" 205 209)
  ("(var2 up)" 209 211)
  ("(var2 stable)" 211 348)
  ("(var2 up)" 348 350)
 )
)
(77
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 111)
  ("(var3 stable)" 111 203)
  ("(var3 up)" 203 208)
  ("(var3 down)" 208 216)
  ("(var3 stable)" 216 218)
  ("(var3 up)" 218 222)
  ("(var3 stable)" 222 368)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 116)
  ("(var4 stable)" 116 206)
  ("(var4 down)" 206 210)
  ("(var4 up)" 210 212)
  ("(var4 down)" 212 327)
  ("(var4 stable)" 327 368)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 114)
  ("(var1 stable)" 114 368)
  ("(var2 stable)" 0 101)
  ("(var2 down)" 101 103)
  ("(var2 stable)" 103 144)
  ("(var2 up)" 144 242)
  ("(var2 down)" 242 245)
  ("(var2 up)" 245 248)
  ("(var2 stable)" 248 368)
 )
)
(78
 (
  ("(var3 down)" 0 2)
  ("(var3 up)" 2 5)
  ("(var3 down)" 5 7)
  ("(var3 stable)" 7 37)
  ("(var3 up)" 37 63)
  ("(var3 stable)" 63 147)
  ("(var3 up)" 147 150)
  ("(var3 down)" 150 160)
  ("(var3 up)" 160 164)
  ("(var3 stable)" 164 298)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 71)
  ("(var4 stable)" 71 179)
  ("(var4 down)" 179 259)
  ("(var4 stable)" 259 298)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 64)
  ("(var1 stable)" 64 298)
  ("(var2 stable)" 0 55)
  ("(var2 down)" 55 59)
  ("(var2 up)" 59 184)
  ("(var2 stable)" 184 298)
 )
)
(79
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 55)
  ("(var3 stable)" 55 57)
  ("(var3 up)" 57 94)
  ("(var3 stable)" 94 169)
  ("(var3 up)" 169 173)
  ("(var3 down)" 173 184)
  ("(var3 up)" 184 189)
  ("(var3 stable)" 189 334)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 43)
  ("(var4 down)" 43 45)
  ("(var4 up)" 45 47)
  ("(var4 down)" 47 49)
  ("(var4 up)" 49 94)
  ("(var4 stable)" 94 199)
  ("(var4 down)" 199 302)
  ("(var4 stable)" 302 334)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 56)
  ("(var1 stable)" 56 60)
  ("(var1 up)" 60 88)
  ("(var1 stable)" 88 334)
  ("(var2 stable)" 0 77)
  ("(var2 down)" 77 79)
  ("(var2 stable)" 79 105)
  ("(var2 up)" 105 115)
  ("(var2 down)" 115 118)
  ("(var2 up)" 118 208)
  ("(var2 stable)" 208 328)
  ("(var2 down)" 328 330)
  ("(var2 stable)" 330 334)
 )
)
(80
 (
  ("(var3 stable)" 0 42)
  ("(var3 up)" 42 75)
  ("(var3 stable)" 75 158)
  ("(var3 up)" 158 163)
  ("(var3 down)" 163 174)
  ("(var3 up)" 174 181)
  ("(var3 stable)" 181 319)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 81)
  ("(var4 stable)" 81 188)
  ("(var4 down)" 188 271)
  ("(var4 stable)" 271 319)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 78)
  ("(var1 stable)" 78 319)
  ("(var2 stable)" 0 64)
  ("(var2 down)" 64 66)
  ("(var2 up)" 66 204)
  ("(var2 stable)" 204 319)
 )
)
(81
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 112)
  ("(var3 stable)" 112 202)
  ("(var3 up)" 202 206)
  ("(var3 down)" 206 216)
  ("(var3 up)" 216 220)
  ("(var3 stable)" 220 364)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 84)
  ("(var4 stable)" 84 86)
  ("(var4 up)" 86 119)
  ("(var4 stable)" 119 210)
  ("(var4 down)" 210 319)
  ("(var4 stable)" 319 364)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 115)
  ("(var1 down)" 115 117)
  ("(var1 stable)" 117 364)
  ("(var2 stable)" 0 102)
  ("(var2 down)" 102 104)
  ("(var2 up)" 104 145)
  ("(var2 stable)" 145 147)
  ("(var2 up)" 147 250)
  ("(var2 stable)" 250 364)
 )
)
(82
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 93)
  ("(var3 stable)" 93 168)
  ("(var3 up)" 168 172)
  ("(var3 down)" 172 182)
  ("(var3 up)" 182 186)
  ("(var3 stable)" 186 317)
  ("(var4 stable)" 0 61)
  ("(var4 up)" 61 94)
  ("(var4 stable)" 94 178)
  ("(var4 down)" 178 275)
  ("(var4 stable)" 275 317)
  ("(var1 stable)" 0 57)
  ("(var1 down)" 57 59)
  ("(var1 up)" 59 88)
  ("(var1 stable)" 88 317)
  ("(var2 stable)" 0 79)
  ("(var2 down)" 79 81)
  ("(var2 up)" 81 200)
  ("(var2 stable)" 200 202)
  ("(var2 up)" 202 205)
  ("(var2 stable)" 205 317)
 )
)
(83
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 60)
  ("(var3 stable)" 60 64)
  ("(var3 up)" 64 95)
  ("(var3 stable)" 95 171)
  ("(var3 up)" 171 176)
  ("(var3 down)" 176 186)
  ("(var3 up)" 186 192)
  ("(var3 stable)" 192 331)
  ("(var4 stable)" 0 61)
  ("(var4 up)" 61 91)
  ("(var4 stable)" 91 186)
  ("(var4 down)" 186 278)
  ("(var4 stable)" 278 331)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 90)
  ("(var1 stable)" 90 331)
  ("(var2 stable)" 0 80)
  ("(var2 down)" 80 84)
  ("(var2 up)" 84 125)
  ("(var2 stable)" 125 127)
  ("(var2 up)" 127 202)
  ("(var2 stable)" 202 331)
 )
)
(84
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 109)
  ("(var3 stable)" 109 111)
  ("(var3 up)" 111 113)
  ("(var3 stable)" 113 187)
  ("(var3 up)" 187 194)
  ("(var3 down)" 194 202)
  ("(var3 up)" 202 209)
  ("(var3 stable)" 209 338)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 122)
  ("(var4 stable)" 122 215)
  ("(var4 down)" 215 305)
  ("(var4 stable)" 305 338)
  ("(var1 stable)" 0 78)
  ("(var1 up)" 78 106)
  ("(var1 stable)" 106 338)
  ("(var2 stable)" 0 98)
  ("(var2 down)" 98 100)
  ("(var2 up)" 100 229)
  ("(var2 stable)" 229 338)
 )
)
(85
 (
  ("(var3 stable)" 0 29)
  ("(var3 up)" 29 85)
  ("(var3 stable)" 85 160)
  ("(var3 up)" 160 164)
  ("(var3 down)" 164 174)
  ("(var3 up)" 174 181)
  ("(var3 stable)" 181 314)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 82)
  ("(var4 stable)" 82 169)
  ("(var4 down)" 169 171)
  ("(var4 up)" 171 174)
  ("(var4 down)" 174 268)
  ("(var4 stable)" 268 314)
  ("(var1 stable)" 0 43)
  ("(var1 up)" 43 76)
  ("(var1 stable)" 76 78)
  ("(var1 up)" 78 80)
  ("(var1 down)" 80 82)
  ("(var1 up)" 82 84)
  ("(var1 stable)" 84 314)
  ("(var2 stable)" 0 68)
  ("(var2 down)" 68 70)
  ("(var2 stable)" 70 107)
  ("(var2 up)" 107 178)
  ("(var2 stable)" 178 314)
 )
)
(86
 (
  ("(var3 stable)" 0 97)
  ("(var3 up)" 97 128)
  ("(var3 stable)" 128 213)
  ("(var3 up)" 213 217)
  ("(var3 stable)" 217 219)
  ("(var3 down)" 219 228)
  ("(var3 up)" 228 230)
  ("(var3 stable)" 230 375)
  ("(var4 stable)" 0 97)
  ("(var4 up)" 97 126)
  ("(var4 stable)" 126 219)
  ("(var4 down)" 219 325)
  ("(var4 stable)" 325 375)
  ("(var1 stable)" 0 97)
  ("(var1 up)" 97 129)
  ("(var1 stable)" 129 375)
  ("(var2 stable)" 0 118)
  ("(var2 down)" 118 122)
  ("(var2 up)" 122 226)
  ("(var2 stable)" 226 375)
 )
)
(87
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 86)
  ("(var3 stable)" 86 157)
  ("(var3 up)" 157 162)
  ("(var3 down)" 162 170)
  ("(var3 stable)" 170 172)
  ("(var3 up)" 172 175)
  ("(var3 down)" 175 177)
  ("(var3 stable)" 177 297)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 81)
  ("(var4 down)" 81 83)
  ("(var4 up)" 83 85)
  ("(var4 down)" 85 87)
  ("(var4 up)" 87 89)
  ("(var4 stable)" 89 177)
  ("(var4 down)" 177 179)
  ("(var4 stable)" 179 181)
  ("(var4 down)" 181 259)
  ("(var4 stable)" 259 297)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 85)
  ("(var1 stable)" 85 297)
  ("(var2 stable)" 0 72)
  ("(var2 down)" 72 74)
  ("(var2 up)" 74 186)
  ("(var2 stable)" 186 297)
 )
)
(88
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 89)
  ("(var3 stable)" 89 168)
  ("(var3 up)" 168 171)
  ("(var3 down)" 171 182)
  ("(var3 up)" 182 188)
  ("(var3 stable)" 188 328)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 89)
  ("(var4 stable)" 89 182)
  ("(var4 down)" 182 283)
  ("(var4 stable)" 283 328)
  ("(var1 stable)" 0 52)
  ("(var1 up)" 52 83)
  ("(var1 stable)" 83 85)
  ("(var1 up)" 85 87)
  ("(var1 stable)" 87 328)
  ("(var2 stable)" 0 75)
  ("(var2 down)" 75 77)
  ("(var2 up)" 77 177)
  ("(var2 down)" 177 179)
  ("(var2 up)" 179 182)
  ("(var2 stable)" 182 328)
 )
)
(89
 (
  ("(var3 stable)" 0 86)
  ("(var3 up)" 86 117)
  ("(var3 stable)" 117 197)
  ("(var3 up)" 197 201)
  ("(var3 down)" 201 211)
  ("(var3 up)" 211 217)
  ("(var3 stable)" 217 352)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 119)
  ("(var4 stable)" 119 237)
  ("(var4 down)" 237 318)
  ("(var4 stable)" 318 352)
  ("(var1 stable)" 0 83)
  ("(var1 up)" 83 115)
  ("(var1 stable)" 115 117)
  ("(var1 up)" 117 120)
  ("(var1 stable)" 120 352)
  ("(var2 stable)" 0 105)
  ("(var2 down)" 105 107)
  ("(var2 up)" 107 217)
  ("(var2 stable)" 217 352)
 )
)
(90
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 111)
  ("(var3 stable)" 111 191)
  ("(var3 up)" 191 193)
  ("(var3 down)" 193 202)
  ("(var3 up)" 202 208)
  ("(var3 stable)" 208 342)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 81)
  ("(var4 stable)" 81 83)
  ("(var4 up)" 83 107)
  ("(var4 stable)" 107 198)
  ("(var4 down)" 198 305)
  ("(var4 stable)" 305 342)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 112)
  ("(var1 stable)" 112 342)
  ("(var2 stable)" 0 98)
  ("(var2 down)" 98 100)
  ("(var2 stable)" 100 132)
  ("(var2 up)" 132 229)
  ("(var2 stable)" 229 342)
 )
)
(91
 (
  ("(var3 stable)" 0 48)
  ("(var3 up)" 48 80)
  ("(var3 stable)" 80 161)
  ("(var3 up)" 161 163)
  ("(var3 down)" 163 173)
  ("(var3 up)" 173 178)
  ("(var3 stable)" 178 310)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 81)
  ("(var4 stable)" 81 181)
  ("(var4 down)" 181 206)
  ("(var4 stable)" 206 208)
  ("(var4 down)" 208 278)
  ("(var4 stable)" 278 310)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 78)
  ("(var1 stable)" 78 310)
  ("(var2 stable)" 0 69)
  ("(var2 down)" 69 71)
  ("(var2 stable)" 71 101)
  ("(var2 up)" 101 198)
  ("(var2 stable)" 198 310)
 )
)
(92
 (
  ("(var3 stable)" 0 95)
  ("(var3 up)" 95 127)
  ("(var3 stable)" 127 215)
  ("(var3 up)" 215 220)
  ("(var3 down)" 220 231)
  ("(var3 up)" 231 238)
  ("(var3 stable)" 238 381)
  ("(var4 stable)" 0 95)
  ("(var4 up)" 95 126)
  ("(var4 stable)" 126 229)
  ("(var4 down)" 229 231)
  ("(var4 up)" 231 233)
  ("(var4 down)" 233 317)
  ("(var4 up)" 317 319)
  ("(var4 down)" 319 321)
  ("(var4 up)" 321 323)
  ("(var4 down)" 323 328)
  ("(var4 stable)" 328 379)
  ("(var4 up)" 379 381)
  ("(var1 stable)" 0 94)
  ("(var1 up)" 94 122)
  ("(var1 stable)" 122 381)
  ("(var2 stable)" 0 115)
  ("(var2 down)" 115 117)
  ("(var2 up)" 117 260)
  ("(var2 stable)" 260 381)
 )
)
(93
 (
  ("(var3 stable)" 0 87)
  ("(var3 up)" 87 127)
  ("(var3 stable)" 127 202)
  ("(var3 up)" 202 208)
  ("(var3 down)" 208 218)
  ("(var3 up)" 218 223)
  ("(var3 stable)" 223 370)
  ("(var4 stable)" 0 89)
  ("(var4 up)" 89 119)
  ("(var4 stable)" 119 212)
  ("(var4 down)" 212 320)
  ("(var4 stable)" 320 370)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 88)
  ("(var1 stable)" 88 90)
  ("(var1 up)" 90 92)
  ("(var1 stable)" 92 94)
  ("(var1 up)" 94 124)
  ("(var1 stable)" 124 370)
  ("(var2 down)" 0 2)
  ("(var2 stable)" 2 110)
  ("(var2 down)" 110 112)
  ("(var2 up)" 112 151)
  ("(var2 stable)" 151 154)
  ("(var2 up)" 154 250)
  ("(var2 stable)" 250 370)
 )
)
(94
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 86)
  ("(var3 stable)" 86 159)
  ("(var3 up)" 159 165)
  ("(var3 down)" 165 174)
  ("(var3 up)" 174 176)
  ("(var3 stable)" 176 303)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 91)
  ("(var4 stable)" 91 175)
  ("(var4 up)" 175 177)
  ("(var4 down)" 177 280)
  ("(var4 stable)" 280 303)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 90)
  ("(var1 stable)" 90 303)
  ("(var2 stable)" 0 100)
  ("(var2 up)" 100 181)
  ("(var2 stable)" 181 303)
 )
)
(95
 (
  ("(var3 stable)" 0 57)
  ("(var3 up)" 57 88)
  ("(var3 stable)" 88 165)
  ("(var3 up)" 165 170)
  ("(var3 stable)" 170 172)
  ("(var3 down)" 172 181)
  ("(var3 up)" 181 184)
  ("(var3 stable)" 184 315)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 94)
  ("(var4 stable)" 94 176)
  ("(var4 down)" 176 276)
  ("(var4 stable)" 276 315)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 90)
  ("(var1 stable)" 90 315)
  ("(var2 stable)" 0 75)
  ("(var2 down)" 75 77)
  ("(var2 stable)" 77 111)
  ("(var2 up)" 111 113)
  ("(var2 stable)" 113 115)
  ("(var2 up)" 115 207)
  ("(var2 stable)" 207 315)
 )
)
(96
 (
  ("(var3 stable)" 0 102)
  ("(var3 up)" 102 128)
  ("(var3 stable)" 128 132)
  ("(var3 up)" 132 134)
  ("(var3 stable)" 134 220)
  ("(var3 up)" 220 223)
  ("(var3 stable)" 223 225)
  ("(var3 down)" 225 237)
  ("(var3 up)" 237 242)
  ("(var3 stable)" 242 386)
  ("(var4 stable)" 0 93)
  ("(var4 up)" 93 95)
  ("(var4 stable)" 95 98)
  ("(var4 up)" 98 127)
  ("(var4 stable)" 127 129)
  ("(var4 up)" 129 132)
  ("(var4 stable)" 132 137)
  ("(var4 up)" 137 139)
  ("(var4 stable)" 139 241)
  ("(var4 down)" 241 357)
  ("(var4 stable)" 357 386)
  ("(var1 stable)" 0 92)
  ("(var1 up)" 92 94)
  ("(var1 stable)" 94 96)
  ("(var1 up)" 96 131)
  ("(var1 stable)" 131 386)
  ("(var2 stable)" 0 120)
  ("(var2 down)" 120 122)
  ("(var2 up)" 122 169)
  ("(var2 stable)" 169 175)
  ("(var2 up)" 175 260)
  ("(var2 stable)" 260 386)
 )
)
(97
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 92)
  ("(var3 down)" 92 94)
  ("(var3 stable)" 94 170)
  ("(var3 up)" 170 175)
  ("(var3 down)" 175 184)
  ("(var3 up)" 184 191)
  ("(var3 stable)" 191 324)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 91)
  ("(var4 down)" 91 93)
  ("(var4 stable)" 93 196)
  ("(var4 down)" 196 279)
  ("(var4 stable)" 279 324)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 97)
  ("(var1 stable)" 97 324)
  ("(var2 stable)" 0 80)
  ("(var2 down)" 80 82)
  ("(var2 stable)" 82 116)
  ("(var2 up)" 116 210)
  ("(var2 stable)" 210 324)
 )
)
(98
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 83)
  ("(var3 stable)" 83 85)
  ("(var3 up)" 85 113)
  ("(var3 stable)" 113 192)
  ("(var3 up)" 192 200)
  ("(var3 down)" 200 210)
  ("(var3 up)" 210 213)
  ("(var3 stable)" 213 351)
  ("(var4 stable)" 0 81)
  ("(var4 up)" 81 113)
  ("(var4 stable)" 113 204)
  ("(var4 down)" 204 206)
  ("(var4 up)" 206 208)
  ("(var4 down)" 208 316)
  ("(var4 stable)" 316 351)
  ("(var1 stable)" 0 82)
  ("(var1 up)" 82 113)
  ("(var1 stable)" 113 351)
  ("(var2 stable)" 0 102)
  ("(var2 down)" 102 106)
  ("(var2 up)" 106 109)
  ("(var2 down)" 109 111)
  ("(var2 up)" 111 215)
  ("(var2 stable)" 215 351)
 )
)
(99
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 53)
  ("(var3 down)" 53 55)
  ("(var3 up)" 55 102)
  ("(var3 stable)" 102 176)
  ("(var3 up)" 176 180)
  ("(var3 stable)" 180 182)
  ("(var3 down)" 182 191)
  ("(var3 up)" 191 196)
  ("(var3 stable)" 196 340)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 105)
  ("(var4 stable)" 105 193)
  ("(var4 up)" 193 196)
  ("(var4 down)" 196 201)
  ("(var4 up)" 201 203)
  ("(var4 down)" 203 292)
  ("(var4 up)" 292 294)
  ("(var4 down)" 294 296)
  ("(var4 stable)" 296 340)
  ("(var1 stable)" 0 57)
  ("(var1 up)" 57 92)
  ("(var1 stable)" 92 340)
  ("(var2 stable)" 0 81)
  ("(var2 down)" 81 85)
  ("(var2 up)" 85 219)
  ("(var2 down)" 219 221)
  ("(var2 up)" 221 224)
  ("(var2 stable)" 224 340)
 )
)
(100
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 86)
  ("(var3 stable)" 86 160)
  ("(var3 up)" 160 165)
  ("(var3 down)" 165 176)
  ("(var3 up)" 176 178)
  ("(var3 stable)" 178 312)
  ("(var4 stable)" 0 52)
  ("(var4 up)" 52 87)
  ("(var4 down)" 87 89)
  ("(var4 up)" 89 91)
  ("(var4 stable)" 91 200)
  ("(var4 down)" 200 267)
  ("(var4 stable)" 267 312)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 84)
  ("(var1 stable)" 84 312)
  ("(var2 stable)" 0 71)
  ("(var2 down)" 71 73)
  ("(var2 stable)" 73 106)
  ("(var2 up)" 106 108)
  ("(var2 stable)" 108 110)
  ("(var2 up)" 110 205)
  ("(var2 stable)" 205 312)
 )
)
